/*
 * ParseFct1.java
 * 
 * Copyright 2004 Christoph Csallner and Yannis Smaragdakis.
 */
package edu.gatech.cc.cnc.firstpass;

import java.util.Map;

import edu.gatech.cc.cnc.Out;
import edu.gatech.cc.cnc.ParseFct;
import edu.gatech.cc.cnc.params.Param;
import edu.gatech.cc.cnc.params.ParamArray;
import edu.gatech.cc.cnc.params.ParamComplex;
import edu.gatech.cc.cnc.params.ParamRefType;


/**
 * ParseFct1
 * 
 * methods specific to first pass.
 * 
 * @author csallner@gatech.edu (Christoph Csallner)
 * @version	$Id: $
 */
public class ParseFct1 extends ParseFct {

 /* StringAndClass
  *
  * Used to propagate the name and class of an param upwards. */
  protected static class IsAVarType { 
  	protected String name = null;
  	protected Class type = null;
  	protected boolean negated = false;  //initially not negated.
  	
  	/* Constructor */
  	IsAVarType(String s, Class c) {
  		assert (s!=null && c!=null);
  		this.name = s; this.type = c;
  	}
  	protected void negate() {negated = !negated;} 
  	protected boolean isNegated() {return negated;}
  	protected String getName() {return name;}
  	protected Class getType() {return type;}
 }

  
  /**
   * Constructor
   */
	public ParseFct1 (Map<String,Param> params) {
		super(params);
	}  
  
	
 /**
  * Apply a type constraint. 
  */
	protected void apply(IsAVarType c) {
    if (c==null) {return;}
    
    if (c.isNegated()) {
    	Out.debug(c.getName()+" is not a "+c.getType().getName());
    	isNotA(c.getName(), c.getType());
    	return;
    }
    
   	Out.debug(c.getName()+" is a "+c.getType().getName());
   	getCreateSpecializeParam(c.getName(), c.getType());
	}
	
	
	/**
	 * name is not a pType
	 */
	protected void isNotA(String name, Class type) {
		Class t = type;  //innermost component type
		
		/* var isNotA int[][] */
		while (t.isArray()) {
			t = t.getComponentType();
		}
		
		/* var isNotA int */
		if (t.isPrimitive()) {
			return;
		}
		
		/* pType is neither primitive nor primitive[] */
		Out.verbose("Ignoring constraint "+getCnt()+": "+
				name+" is not a "+type.getName());
		/* TODO */
	}
	
	
	/**
	 * @return an object containing variable v's name and type.
	 */
	protected IsAVarType isA(String v, String t) {
    if (v==null || t==null) {return null;}
    
    Class tType = getType(t);
    if (tType==null) {return null;}
    
    return new IsAVarType(v, tType);		
	}

	/**
	 * @return an object containing variable v's name and type.
	 */
	protected IsAVarType isAExprTypeOfApp(String v, String t) {
		if (v==null || t==null) {return null;}
		
    Param param = params.get(t);
    if (param==null) {return null;}
    
    return isA(v, param.getTypeName());
	}  	

	
	/* @return type encoding in arrays according to Class.getName(), e.g.
	 * refType ::= L<classname>;
	 * int     ::= I */
	private String getTypeEncoding(String s) {
		if (s.equals("int"))  	{return "I";}
		if (s.equals("long"))   {return "J";}
		if (s.equals("boolean")){return "Z";}
		if (s.equals("short"))  {return "S";}
		if (s.equals("byte")) 	{return "B";}
		if (s.equals("char")) 	{return "C";}
		if (s.equals("float")) 	{return "F";}
		if (s.equals("double")) {return "D";}
		return "L" +s +";";  //default
	}

	
	/**
	 * (array int) | (array java.lang.String)
	 * 
	 * @return array type componentName of dimensionality one.
	 */
	protected String getArrayEncoding(String componentName) {
		assert componentName!=null;
		
		return "[" +getTypeEncoding(componentName);		
	}		


	/**
	 * byte | [[int | [Ljava.lang.Object; | TypeTestee$B
	 * 
	 * @returns null iff s denotes a JML type.
	 */
	private Class getType(String s) {		
		if (s.equals("int"))  	{return Integer.TYPE;}
		if (s.equals("long"))   {return Long.TYPE;}
		if (s.equals("boolean")){return Boolean.TYPE;}
		if (s.equals("short"))  {return Short.TYPE;}
		if (s.equals("byte")) 	{return Byte.TYPE;}
		if (s.equals("char")) 	{return Character.TYPE;}
		if (s.equals("float")) 	{return Float.TYPE;}
		if (s.equals("double")) {return Double.TYPE;}
 
		/* Follow ESC's treatment of JML types
		 * [ESC 2.0a8 Implementation notes, chapter 3.16.3: New JML types] */
		if (s.equals("bigint")) {return Long.TYPE;}  
		if (s.equals("real")) {return Double.TYPE;}	
		
		/* Ignore remaining non-Java types */
		if (s.equals("arrayType") || s.equals("anytype")) {
			return null;
		}
		
		/* Reference type */
		try {
			return Class.forName(s);
		}
		catch(Exception e) {
			Out.verbose("Could not resolve type " +s +", ignoring constraint " +getCnt());
			return null;
		}
	}

	
	/**
	 * @return ::= Param | null;
	 */
	protected Param getCreateParam(String v, Class<?> c) {
		if (v==null) {return null;}
		
		Param param = params.get(v);
		if (param!=null) {return param;}  //hit
		
		/* Not yet inserted */
		if (c==null) {return null;}
		
		param = createParam(c, v);
		addParam(v, param);
		return param;
	}
	
	
	/**
	 * (o:26.19, HeapNode)
   * 
	 * @return Param
	 */
	protected Param getCreateSpecializeParam(String v, Class<?> c) {
		if (v==null || c==null) {return null;}
		
		Param param = getCreateParam(v, c);
		if (param==null) {return null;}
		
		if (param.getType().isAssignableFrom(c) && !param.getType().equals(c)) {
			/* c is a subtype of param's type */
			if (c.isArray()) {
				specialize((ParamRefType)param, new ParamArray(c, param.toString()));
			}
			else {
				((ParamComplex) param).specializeTo(c);
			}
		}

		return param;	
	}
	
	
	/** 
	 * @param var ::= Param | varName | null;
	 * @return ::= typeName | null;
	 */ 
	public String array(Object var) {
		if (var==null) {return null;}
		
		Param p;		
		if (var instanceof Param) {
			p = (Param) var;
		}
		else {
			p = getCreateParam((String)var, (Class)null);
		}
				
		if (p==null) 
			return null;
		
		return getArrayEncoding(p.getType().toString());
	}	
	
	
	protected void specialize(ParamRefType pOld, ParamArray pNew) {
		/* remove records on pOld */
		params.remove(pOld.toString());
		addParam(pNew.toString(), pNew);
		ParamRefType.getEq().replace(pOld, pNew);
	}
}
